open InsertSort 

module P = struct
  let rec to_int32 = function
  | XI p -> Int32.add (Int32.shift_left (to_int32 p) 1) 1l
  | XO p -> Int32.shift_left (to_int32 p) 1
  | XH -> 1l

  let rec of_int32 n =
    if Int32.logand n 1l = 0l then
      if n = 0l
      then assert false
      else XO (of_int32 (Int32.shift_right_logical n 1))
    else
      if n = 1l
      then XH
      else XI (of_int32 (Int32.shift_right_logical n 1))
end

module Z = struct
  let of_int32 n =
    if n = 0l then Z0 else
    if n > 0l then Zpos (P.of_int32 n)
    else Zneg (P.of_int32 (Int32.neg n))

  let to_int32 = function
  | Z0 -> 0l
  | Zpos p -> P.to_int32 p
  | Zneg p -> Int32.neg (P.to_int32 p)
end

let coqz_of_camlint : int32 -> InsertSort.z = Z.of_int32
let camlint_of_coqz : InsertSort.z -> int32 = Z.to_int32

let rec coqlistz_of_camllistint list_int32 =
  match list_int32 with
   [] -> InsertSort.Nil
  | head :: tail -> let coqlisthead = coqz_of_camlint head in
                    let coqlisttail = coqlistz_of_camllistint tail in 
                    InsertSort.Cons(coqlisthead, coqlisttail)

let rec camllistint_of_coqlistz list_coqz =
  match list_coqz with
  InsertSort.Nil -> []
  | InsertSort.Cons(head, tail) -> let camllisthead = camlint_of_coqz head in
                                   let camllisttail = camllistint_of_coqlistz tail in
                                   camllisthead :: camllisttail

